COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Proposed revision of chapter PROVIN
C00006 ENDMK
C⊗;
Proposed revision of chapter PROVIN

1. Begin with a short introduction about proving computer programs.
Actually the present introduction is ok.
It should be emphasized that the chapter presents techniques and
not proofs of theorems about recursive Lisp programs in general.

2. First order logic.  An informal introduction starting with the
example of a theory of kinship.  Mainly it presupposes as fixed
theory with a fixed domain, but a the end it mentions that theories
can have more than one interpretation.  Starting with a fixed
interpretation simplifies the presentation and allows considering
sentences as asserting facts.  In the main in LISP program proving,
we are dealing with fixed interpretations anyway.  The general
mathematical presentation that develops syntax first and then
introduces interpretations is difficult for beginners.

3. The theory of S-expressions and lists.  This theory which is
analogous to arithmetic has only the operators of LISP.
Mention the decideability of the theory.  Probably one shold then
mention append or istail and a few of the properties of the more
general theory.  The S-expression and Lisp axiom schemata are mentioned
at this point.  I don't know whether the idea of proofs using
orderings should be done here.  Maybe orderings should be a separate
section after section 4.

4. Proof of properties of programs known to terminate.  We appeal to
the theorem that we can then introduce a function symbol.  At this
point we have the example of append.  However, the example is
considered to be correct and not just tentative.  Other examples
can be given.

5. Translating programs not known to terminate.  The functional
equation and the minimization schema.  The imitation boolean
operators.  Proofs of termination of append.

6. Orderings and induction.  The samefringe example and Ackermann
could be done here.

Actually, the main revision of current material required is the
informal introd to first order logic.
Maybe less would be needed than I have thought.